An ongoing problem in the design of large systems is verifying that the system will behave in the manner intended by its designers. One approach has been to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Since there is no guarantee that an untested system will work as expected, building the system itself can be an expensive proposition. Thus, those skilled in the art have migrated toward building and testing a model of the system, or system model, through software.
A system model can be said to be a computer program or block of code that, when executed, simulates the intended properties, or functions, of the system. Basically, the system model is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. To do this, the system model uses variables, called system-model variables, that are programmed within the code to take on certain values depending on the values of the inputs to the system model. That is, as different values are fed to the system-model inputs, the system-model variables are assigned different values that indicate how the system model functions or behaves in response to the inputs. Thus, by controlling the value of the inputs to the system model and monitoring the values of the system-model variables, a system designer can test or observe the behavior of the system model in response to different sets of inputs, and determine whether the system model exhibits, or performs, the intended behaviors or properties of the system.
One method of testing a system model in such a manner is called formal verification. In formal verification, a verification tool is used to convert the system model into a finite state machine. A finite state machine is a set of states and state transitions which minimic the operation of the system model in response to given sets of inputs, or input vectors. In general, each state of a finite state machine represents a specific assignment of values to a set of system-model variables and/or inputs, and thus represents a specific behavior or property of the system model. Each state transition defines the values that a set of system-model variables and/or inputs must take on for the state machine to transition from one state to another state. The state machine thereby provides a roadmap of how a system model will behave (i.e. the states the system model will enter) in response to the values input to the system-model inputs. As a result, once the verification tool converts the system model into such a finite state machine, the tool can test the properties or behaviors of the system model by checking which states the system-model state machine enters in response to a given set of inputs.
To illustrate, conventional verification tools, such as the verification tool described by R. P. Kurshan in Computer Aided Verification of Coordinating Processes, Princeton University Press 1994, are designed to test all the properties or behaviors of a system model by performing a so-called full search of the system-model state space (i.e. the set of states and state transitions that form the system-model state machine). Conventionally, the verification tool begins the full search by inputting a "complete set of inputs" at a set of initial states, or "set of reset states," of the system-model state machine. The term "complete set of inputs" as used herein refers to every possible set of values that the system-model inputs can possibly assume when the system model is in operation, in every possible sequence. The term "set of reset states" as used herein refers to those states from which the system model is designed to begin operation and/or return to after an operation is completed.
As the complete set of inputs are fed to the state machine at the set of reset states, the verification tool identifies the values that the system-model variables and/or inputs take on, and identifies the state transitions that are enabled by those values. Once the enabled state transitions are identified, the verification tool identifies the states, called "next states," to which the state machine can transition as a result of the inputs. Once the verification tool identifies all the next states that are reached as a result of the inputs, it continues the search by inputting the complete set of inputs at each of the next states and by identifying the new set of next states to which the state machine transitions as a result of the inputs. This process is repeated until the set of next states identified by the verification tool are all states that have already been reached (i.e. identified as next states) during the search. The set of states that are reached during the search are hereinafter referred to as the set of reachable states. By inputting the complete set of inputs at each state of the state machine, the set of reachable states is guaranteed to include every state of the system-model state space. As a result, the verification tool performing a full search is guaranteed to check every property or behavior of the system model.
In some instances, however, a system designer may wish to check only a portion of the properties or behaviors of a system model. For example, in some instances, the system designer may wish to check the system-model properties that conform with a subset of the inputs that may be possible during the operation of the system. In such instances, it is not necessary to search or reach all of the states of the system-model state machine, and thus it is not necessary to check the behavior of the system-model state machine in response to the complete set of inputs. Instead, the verification tool only needs to search or reach those states that represent the properties or behaviors the designer wishes to check, and thus only needs to check the behavior of the system-model state machine in response to a fraction of the complete set of inputs.
One method for directing the verification tool to check only a portion of the properties or behaviors of the system-model is to program the verification tool with so-called constraints. A constraint is a logical expression composed of an enabling condition and an assumption. The enabling condition defines the condition that must be true for the assumption to be invoked. The assumption defines the value or values that the verification tool shall assign to certain system-model variables and/or inputs when the enabling condition is true. An enabled constraint can therefore direct the verification tool to assign certain values to certain system-model variables and/or inputs, regardless of the values they are programmed to take on within the system-model.
When programmed with such a constraint, the verification tool will be directed to recognize only those state transitions that require the system-model variables and/or inputs to take on values that are consistent with the values defined by the constraints. As a result, the verification tool will only reach those states that represent an assignment of values (i.e. values of the system-model variables and inputs) that are consistent with the values defined by the constraint. Thus, by carefully choosing the values which the constraint assigns to certain system-model variables and inputs, the verification tool can be directed to reach or search only those states that represent the properties or behaviors which the system-designer wishes to check.
For example, the constraint "IF(power-on)Assume(x=y)" will direct a verification tool to assume that the value of system-model variable x equals the value of system-model variable y when the enabling condition, power.sub.-- on, is true. Once enabled, the constraint will direct the verification tool to only search or reach those states or state transitions where the inputs cause the value of system-model variable x to be equal to the value of system-model variable y. The constraint therefore defines a specific set of reachable states for the verification tool. Thus, if the specific set of reachable states includes all the states that represent the system-model property being checked, the constraint is said to properly limit the search.
Oftentimes, the system designer is required to program the verification tool with a plurality of constraints in order to properly limit the search. When programmed with a plurality of constraints, the verification tool will only search or reach the states that are consistent with every value defined by every constraint enabled in that state. Thus, it is important that the constraints enabled in each state assign values that properly define the set of reachable states.
A problem occurs, however, when the constraints enabled in a given state assign values that are inconsistent with each other. Such a set of enabled constraints are said to be mutually-contradictory at the given state. For example, the set of constraints:
Constraint1=IF(power-on)Assume (x=y); Constraint2=
IF(temperature&gt;30)Assume(y-z); and Constraint3=IF(time&gt;1)Assume(x.noteq.z); are mutually contradictory at any state in which all the enabling conditions are true at the same time. To illustrate, at a state wherein power.sub.-- on, temperature&gt;30, and time&gt;1 are all true, Constraints 1-3 will direct the verification tool to assume x=y=z.noteq.x, or x.noteq.x, which is inconsistent, and thus mutually contradictory.
When a set of constraints are mutually contradictory (i.e. assign inconsistent values) at a given state of the search, the system-model variables and/or inputs can not take on a set of values that would be consistent with the values assigned by every enabled constraint at the same time. As a result, the verification tool performing the search will not recognize any state transition from that given state to any other state, no matter what inputs are fed to the state machine. This means that the verification tool will not reach or search any states beyond the given state in which the mutually contradictory constraints are enabled. As a result, the verification tool may fail to reach all the states associated with the system-model property or behavior being checked. When this happens the verification tool may not be able to identify all the errors associated with the property being checked. Thus, in order to check whether a verification tool's report of "no error" is accurate, the system designer should always check whether the set of constraints input to the verification tool are mutually contradictory.
A related and more subtle version of this problem occurs when the constraints, although not mutually contradictory at a single state, are inconsistent with each other in a group of states. A set of constraints are inconsistent in a group of states when the values assigned by constraints enabled in the group of states direct the verification tool to perpetually search only the states in the group. When this happens, the verification tool performing the search will not recognize any state transition from the group of states to any other state or group of states, no matter what inputs are fed to the state machine. This means that the verification tool will not reach or search any states beyond the given group of states in which the inconsistent constraints are enabled. As a result, the verification tool may fail to reach all the states associated with the system-model property or behavior being checked, and thus the verification tool may not be able to identify all the errors associated with the property being checked. When this happens, the constraints are said to "overconstrain" the search of the system-model state space. Thus, in addition to checking whether a set of constraints are mutually contradictory in a single state to determine whether a verification tool's report of "no error" is accurate, the system designer should also check whether the set of constraints assign inconsistent values in a group of states.
The conventional method for determining whether a set of constraints input to a verification tool are mutually contradictory at a single state or are inconsistent in a group of states is to analyze all the assumptions (i.e. value assignments) defined by all of the constraints. The object of such an analysis is to determine whether it is possible for the values assigned by one constraint to be inconsistent with the values assigned by another constraint at each state and each group of states. This requires that the values assigned by each constraint be analyzed for consistency with the values assigned by every other constraint at each state and each group of states of the state machine. Since some constraints may assign values as a function of other variables and/or inputs in each state, such an analysis requires a detailed understanding and/or determination of the mathematical relationship between the system-model variables and/or inputs, and an understanding or determination of the set of values that the system-model variables and/or inputs can assume in response to any given set of inputs at each state of the system-model state space. For systems having a large number of states and/or a large number of variables and inputs, such a task can be very time-consuming and can require a large amount of computational resources.